Search Results

There has been work on the strength of semi-classical axioms over Heyting arithmetic such as Σ_n-DNE (double negation elimination) and Π_n-LEM (law of excluded middle). Among other things, Akama et al. show that Σ_n-DNE does not imply Π_n-LEM for any n ≥ 1 by using Kleene realizability relativized to Turing degrees. These realizability notions are expressed by subtoposes of the effective topos ℰff and thus by corresponding local operators (a.k.a. Lawvere-Tierney topologies). Our purpose is to provide a topos-theoretic explanation for separation of semi-classical axioms. It consists of determining the least dense local operator of a given axiom φ in a topos ℰ, which completely characterizes the dense subtoposes of ℰ satisfying φ. This idea is motivated by Caramello’s study of intermediate propositional logics and van Oosten’s study of Lifschitz realizability. We first investigate sufficient conditions for an arithmetical formula to have a least dense operator. In particular, we show that each semi-classical axiom has a least dense operator in every elementary topos with natural number object. This is a generalization of van Oosten’s result for Π₁∨Π₁-DNE in ℰff. We next determine least dense operators of semi-classical axioms in ℰff in terms of (generalized) Turing degrees. Not only does it immediately imply some separation results of Akama et al. but also explain that realizability notions they used are optimal in the sense of minimality. We finally point out a negative consequence that Π_n-LEM, Σ_n-LEM and Σ_{n+1}-DNE are never separable by any subtopos of ℰff for any n ≥ 0.